package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeSet;

import org.apache.log4j.Logger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.xplain.Xplain;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.SynsetSet;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Config;
import edu.uic.cs.cs582.misc.GeneralException;
import edu.uic.cs.cs582.misc.LogHelper;
import edu.uic.cs.cs582.process.SatProcessor;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.SynsetIndex;
import edu.uic.cs.cs582.process.impl.SatIndexParser.WordIndex;

public class SatProcessorImplKeepingMiddleVariables implements SatProcessor
{
	private static final Logger LOGGER = LogHelper
			.getLogger(SatProcessorImplKeepingMiddleVariables.class);

	private Xplain<ISolver> solver = null;

	private TreeSet<Integer> conflictSynsetIndexes = new TreeSet<Integer>();
	private TreeSet<Integer> conflictWordIndexes = new TreeSet<Integer>();

	private Component component = null;

	private int[] conflictClauseIndices = null;

	public SatProcessorImplKeepingMiddleVariables(Component component)
	{
		this.component = component;
	}

	private int[][] convertCnfIntoIntArrays(Set<int[]> cnf)
	{
		int[][] result = cnf.toArray(new int[cnf.size()][]);
		return result;
	}

	@Override
	/*public boolean processSat(int[][] cnfClauses) throws TimeoutException*/
	public boolean processSat(Map<int[], Index> indicesByCnfClause)
			throws TimeoutException
	{
		int[][] cnfClauses = convertCnfIntoIntArrays(indicesByCnfClause
				.keySet());

		System.out.println("================================");
		//		System.out.println("p cnf " + cnfClauses.length);
		for (int clause[] : cnfClauses)
		{
			for (int variable : clause)
			{
				System.out.print(variable + " ");
			}
			System.out.println("0");
		}
		System.out.println("================================");

		initializeSolver(cnfClauses);

		initializeClauses(cnfClauses, indicesByCnfClause);

		// if there's conflict happening when add variables into the solver,
		// return false, and there's no need for further checking
		if (!conflictSynsetIndexes.isEmpty() || !conflictWordIndexes.isEmpty())
		{
			return false;
		}

		LOGGER.debug("Begin to solve SAT. ");
		boolean result = solver.isSatisfiable();
		LOGGER.debug("End to solve SAT. Result is [" + result + "]. ");

		if (!result)
		{
			gatherConflictVariablse(cnfClauses, indicesByCnfClause);
		}

		return result;
	}

	private void gatherConflictVariablse(int[][] cnfClauses,
			Map<int[], Index> indicesByCnfClause) throws TimeoutException
	{
		List<int[]> conflictClauses = getConflictClauses(cnfClauses);
		for (int[] clause : conflictClauses)
		{
			for (int variable : clause)
			{
				System.out.print(variable + " ");
			}
			System.out.println("0");

			mapAndStoreConflictVariables(clause, indicesByCnfClause);
		}
	}

	// 'package access' for test use
	List<int[]> getConflictClauses(int[][] cnfClauses) throws TimeoutException
	{
		if (conflictClauseIndices == null)
		{
			conflictClauseIndices = solver.minimalExplanation();
		}

		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_ONE + "Conflict clause indices: "
					+ Arrays.toString(conflictClauseIndices));
		}

		ArrayList<int[]> result = new ArrayList<int[]>(
				conflictClauseIndices.length);
		for (int index : conflictClauseIndices)
		{
			if (LOGGER.isDebugEnabled())
			{
				LOGGER.debug(LogHelper.LOG_LAYER_TWO + "Conflict clause: "
						+ Arrays.toString(cnfClauses[index - 1]));
			}

			result.add(cnfClauses[index - 1]);

		}

		return result;
	}

	private void initializeClauses(int[][] cnfArrays,
			Map<int[], Index> indicesByCnfClause)
	{
		conflictClauseIndices = null;
		solver.reset();

		VecInt vecInt = new VecInt();
		for (int[] clause : cnfArrays)
		{
			try
			{
				for (int variable : clause)
				{
					vecInt.push(variable);
				}
				solver.addClause(vecInt);
				vecInt.clear();
			}
			catch (ContradictionException e)
			{
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_ONE_BEGIN
							+ "Early conflict detected. ");
				}

				mapAndStoreConflictVariables(clause, indicesByCnfClause);

				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_ONE_END
							+ "Early conflict detected. ");
				}
			}
		}
	}

	// 'package access' for test use
	void mapAndStoreConflictVariables(int[] clause,
			Map<int[], Index> indicesByCnfClause)
	{
		Index index = indicesByCnfClause.get(clause);
		if (index instanceof WordIndex)
		{
			conflictWordIndexes.add(((WordIndex) index)
					.getWordIndexInOneComponent());
			if (LOGGER.isDebugEnabled())
			{
				LOGGER.debug(LogHelper.LOG_LAYER_TWO
						+ "Conflict Word: "
						+ component.getWordByIndex(((WordIndex) index)
								.getWordIndexInOneComponent()));
			}
		}
		else if (index instanceof SynsetIndex)
		{
			conflictSynsetIndexes.add(((SynsetIndex) index).getSynsetIndex());
			if (LOGGER.isDebugEnabled())
			{
				LOGGER.debug(LogHelper.LOG_LAYER_TWO
						+ "Conflict Synset: "
						+ component.getSynsetByIndex(((SynsetIndex) index)
								.getSynsetIndex()));
			}
		}
		/*else if (index instanceof SynsetAndWordIndex)
		{
			conflictWordIndexes.add(((SynsetAndWordIndex) index)
					.getWordIndexInOneComponent());
			conflictSynsetIndexes.add(((SynsetAndWordIndex) index)
					.getSynsetIndex());
			if (LOGGER.isDebugEnabled())
			{
				LOGGER.debug(LogHelper.LOG_LAYER_TWO
						+ "Conflict Synset: "
						+ component
								.getSynsetByIndex(((SynsetAndWordIndex) index)
										.getSynsetIndex())
						+ " and Conflict Word: "
						+ component.getWordByIndex(((SynsetAndWordIndex) index)
								.getWordIndexInOneComponent()));
			}
		}*/
		else
		{
			throw new GeneralException(
					"Should find a index for the specified CNF clause! ");
		}
	}

	/*// 'package access' for test use
	void mapAndStoreConflictVariables(int[] clause,
			Map<int[], Index> cnfClausesByIndex)
	{
		for (int variable : clause)
		{
			Index index = SatIndexParser.parseIndex(variable, component);
			if (index instanceof SynsetIndex)
			{
				conflictSynsetIndexes.add(((SynsetIndex) index)
						.getSynsetIndex());
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_TWO
							+ variable
							+ " : Conflict Synset: "
							+ component.getSynsetByIndex(((SynsetIndex) index)
									.getSynsetIndex()));
				}
			}
			else if (index instanceof WordIndex)
			{
				conflictWordIndexes.add(((WordIndex) index)
						.getWordIndexInOneComponent());
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_TWO
							+ variable
							+ " : Conflict Word: "
							+ component.getWordByIndex(((WordIndex) index)
									.getWordIndexInOneComponent()));
				}
			}
		}
	}*/

	private void initializeSolver(int[][] cnfArrays)
	{
		solver = new Xplain<ISolver>(SolverFactory.newDefault());

		solver.setTimeoutMs(Config.TIMEOUT);
		solver.setDBSimplificationAllowed(true);
		solver.newVar(Config.MAXVAR);
		solver.setExpectedNumberOfClauses(cnfArrays.length);
	}

	private Set<Synset> getConflictSynset()
	{
		HashSet<Synset> result = new HashSet<Synset>(
				conflictSynsetIndexes.size());
		for (Integer index : conflictSynsetIndexes)
		{
			result.add(component.getSynsetByIndex(index));
		}

		//		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = initializeConflictingSynsetsSet();
		//		for (SynsetSet set : conflictingWordsByMajoritySynsets.keySet())
		//		{
		//			result.addAll(set);
		//		}

		return result;
	}

	/*public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();

		boolean hasChanged = false;
		do
		{
			hasChanged = false;

			for (Word word : allWords)
			{
				if (isWordContainsNonConflictMajoritySynset(word,
						allConflictSynsets))
				{
					continue;
				}

				if (!hasChanged
						&& allConflictSynsets.addAll(word
								.getAllSynsetsInMajoritySynsets()))
				{
					hasChanged = true;
				}

				for (Synset conflictingSynset : word
						.getAllSynsetsInMajoritySynsets())
				{
					//					if (isOneMajoritySynsetContainsGivenSynset(word,
					//							conflictingSynset))
					//					{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
					//					}
				}

			}
		}
		while (hasChanged);

		// post-process, remove all conflict list contain only one word
		Iterator<Entry<Synset, Set<Word>>> iterator = result.entrySet()
				.iterator();
		while (iterator.hasNext())
		{
			Set<Word> words = iterator.next().getValue();
			if (words.size() == 1)
			{
				iterator.remove();
			}
		}

		return result;
	}*/

	@Override
	public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();

		//		if (allConflictSynsets.isEmpty())
		//		{
		//			return result;
		//		}

		for (Word word : allWords)
		{
			if (isWordContainsNonConflictMajoritySynset(word,
					allConflictSynsets))
			{
				continue;
			}

			// here, all majority-synsets contain some conflict synset
			// we need to get a map to tell which word has which synsets
			for (Synset conflictingSynset : allConflictSynsets)
			{
				if (doesAnyMajoritySynsetContainGivenSynset(word,
						conflictingSynset))
				{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
				}
			}
		}

		//		Map<Synset, Set<Word>> resultFromConflictWords = getConflictWordsBySynsetsInMajority();
		//		result = combineTwoResult(result, resultFromConflictWords);

		//		Iterator<Entry<Synset, Set<Word>>> iter = result.entrySet().iterator();
		//		while (iter.hasNext())
		//		{
		//			Entry<Synset, Set<Word>> entry = iter.next();
		//			if (entry.getValue().size() == 1)
		//			{
		//				iter.remove();
		//			}
		//		}

		return result;
	}

	//	private Map<Synset, Set<Word>> combineTwoResult(
	//			Map<Synset, Set<Word>> result,
	//			Map<Synset, Set<Word>> resultFromConflictWords)
	//	{
	//		for (Entry<Synset, Set<Word>> entry : resultFromConflictWords
	//				.entrySet())
	//		{
	//			Synset keySynset = entry.getKey();
	//			if (!result.containsKey(keySynset))
	//			{
	//				result.put(keySynset, new HashSet<Word>());
	//			}
	//			result.get(keySynset).addAll(entry.getValue());
	//		}
	//
	//		return result;
	//	}

	private boolean isWordContainsNonConflictMajoritySynset(Word word,
			Set<Synset> allConflictSynsets)
	{
		for (Set<Synset> eachMajority : word.getMajoritySynsets())
		{
			boolean isMajorityContainsConflict = false;
			for (Synset eachConflictSynset : allConflictSynsets)
			{
				if (eachMajority.contains(eachConflictSynset))
				{
					isMajorityContainsConflict = true;
					break;
				}
			}

			if (!isMajorityContainsConflict)
			{
				return true;
			}
		}

		return false;
	}

	private boolean doesAnyMajoritySynsetContainGivenSynset(Word word,
			Synset conflictingSynset)
	{
		for (SynsetSet eachMajoritySynsets : word.getMajoritySynsets())
		{
			if (eachMajoritySynsets.contains(conflictingSynset))
			{
				return true;
			}
		}

		return false;
	}

	@Override
	public Map<SynsetSet, Set<Word>> getConflictWordsBySynsetsInMajority()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynset = initializeConflictingSynsetsSet();
		Set<SynsetSet> allKnownConflictingMajoritySynsets = conflictingWordsByMajoritySynset
				.keySet();

		for (Word word : component.getAllWords())
		{
			Integer wordIndex = component.getIndexOfWord(word);
			if (conflictWordIndexes.contains(wordIndex))
			{
				// the conflicting words that have already processed in above steps
				continue;
			}

			if (isWordConflictingInAllItsMajoritySynsets(word,
					allKnownConflictingMajoritySynsets))
			{
				conflictWordIndexes.add(wordIndex);
				for (SynsetSet majoritySynset : word.getMajoritySynsets())
				{
					Set<Word> conflictingWords = conflictingWordsByMajoritySynset
							.get(majoritySynset);
					if (conflictingWords == null)
					{
						conflictingWords = new TreeSet<Word>();
						conflictingWordsByMajoritySynset.put(majoritySynset,
								conflictingWords);
					}
					conflictingWords.add(word);
				}
			}
		}

		return conflictingWordsByMajoritySynset;
	}

	private boolean isWordConflictingInAllItsMajoritySynsets(Word word,
			Set<SynsetSet> allKnownConflictingMajoritySynsets)
	{
		List<SynsetSet> allMajoritySynsetsOfWord = word.getMajoritySynsets();
		return allKnownConflictingMajoritySynsets
				.containsAll(allMajoritySynsetsOfWord);

		/*// if word has only one majority, 
		// and the only one has common with any known conflict SynsetSet of some majority
		if (allMajoritySynsetsOfWord.size() == 1)
		{
			SynsetSet theOnlyOneMajority = allMajoritySynsetsOfWord.get(0);
			return allKnownConflictingMajoritySynsets
					.contains(theOnlyOneMajority);
			*//**
			* Can not only use common!
			* 
			* NEGATIVE=[
			* oppression_{SID-07538674-N=0.1, SID-13996719-N=0.1, SID-00421047-N=1.0}, 
			* oppressiveness_{SID-07538674-N=0.1, SID-04711031-N=0.1}, 
			* subjection_{SID-00089027-N=0.1, SID-13996300-N=0.1}, 
			* subjugation_{SID-00089027-N=0.1, SID-00421047-N=0.1, SID-13996300-N=1.0}], 
			* 
			* POSITIVE=[conquest_{SID-00065216-N=1.0, SID-00089027-N=2.0, SID-00160532-N=0.1}]}
			* 
			* >>>>>>>>* conquest[POSITIVE]  -- [SID-00089027-N]
			* >>>>>>>>* subjection[NEGATIVE]  -- [SID-00089027-N, SID-13996300-N]
			* >>>>>>>>* subjugation[NEGATIVE]  -- [SID-13996300-N]
			*/
		/*
		for (SynsetSet knownConflictingSynsetSet : allKnownConflictingMajoritySynsets)
		{
		if (knownConflictingSynsetSet.hasCommon(theOnlyOneMajority))
		{
			return true;
		}
		}
		}
		// if word has more than one majorities, 
		// make sure all of them are equal to some known conflict SynsetSet of some majority 
		//		else
		//		{
		//			return allKnownConflictingMajoritySynsets
		//					.containsAll(allMajoritySynsetsOfWord);
		//		}

		return false;*/
	}

	//	private Set<Synset> getAllConflictSynsets(
	//			Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets)
	//	{
	//		Set<Synset> result = new HashSet<Synset>();
	//		for (SynsetSet set : conflictingWordsByMajoritySynsets.keySet())
	//		{
	//			result.addAll(set);
	//		}
	//
	//		return result;
	//	}

	/*// @Override
	public Map<SynsetSet, Set<Word>> getConflictWordsByMajoritySynsets2()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = initializeConflictingSynsetsSet();

		//		boolean hasChanged = false;
		//		do
		//		{
		//			hasChanged = false;

		for (Word word : component.getAllWords())
		{
			Integer otherWordIndex = component.getIndexOfWord(word);
			if (conflictWordIndexes.contains(otherWordIndex))
			{
				// the conflicting words that have already processed in above steps
				continue;
			}

			// if one word has only one majority-synset, 
			// and the majority-synset has common with some known as inconsistent
			SynsetSet commonSynsetSet = getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
					word, conflictingWordsByMajoritySynsets);
			if (commonSynsetSet != null)
			{
				conflictWordIndexes.add(otherWordIndex);
				Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
						.get(commonSynsetSet);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					conflictingWordsByMajoritySynsets.put(commonSynsetSet,
							conflictingWords);
					//						hasChanged = true;
				}
				conflictingWords.add(word);

				continue;
			}

			// the words that haven't been reported, but may be the cause of conflict

			// if word doesn't have free majority-synsets
			// the word must be inconsistent
			if (!hasConflictFreeMajoritySynsets(word,
					conflictingWordsByMajoritySynsets))
			{
				conflictWordIndexes.add(otherWordIndex);

				for (SynsetSet majoritySynsetsOfWord : word
						.getMajoritySynsets())
				{
					Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
							.get(majoritySynsetsOfWord);
					if (conflictingWords == null)
					{
						conflictingWords = new TreeSet<Word>();
						conflictingWordsByMajoritySynsets.put(
								majoritySynsetsOfWord, conflictingWords);
						//							hasChanged = true;
					}
					conflictingWords.add(word);
				}
			}
		}
		//		}
		//		while (hasChanged);

		return conflictingWordsByMajoritySynsets;
	}

	private SynsetSet getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
			Word word,
			Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets)
	{
		for (Entry<SynsetSet, Set<Word>> knownConflicting : conflictingWordsByMajoritySynsets
				.entrySet())
		{
			SynsetSet conflictingMajoritySynsets = knownConflicting.getKey();
			List<SynsetSet> allMajoritySynsetsOfTheWord = word
					.getMajoritySynsets();
			if (allMajoritySynsetsOfTheWord.size() == 1
					&& allMajoritySynsetsOfTheWord.get(0).hasCommon(
							conflictingMajoritySynsets))
			{
				return allMajoritySynsetsOfTheWord.get(0);
			}
		}

		return null;
	}*/

	// if a word is said to be inconsistent, all its majority-synsets must be inconsistent, 
	// otherwise the certain polarity can be assigned to that 'conflict-free' majority-synsets 
	private Map<SynsetSet, Set<Word>> initializeConflictingSynsetsSet()
	{
		Map<SynsetSet, Set<Word>> result = new HashMap<SynsetSet, Set<Word>>();

		// for each conflicting word
		List<Integer> conflictIndexList = new ArrayList<Integer>(
				conflictWordIndexes);

		for (Integer wordIndex : conflictIndexList)
		{
			Word conflictingWord = component.getWordByIndex(wordIndex);
			for (SynsetSet majoritySynset : conflictingWord
					.getMajoritySynsets())
			{
				Set<Word> conflictingWords = result.get(majoritySynset);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					result.put(majoritySynset, conflictingWords);
				}
				conflictingWords.add(conflictingWord);
			}
		}

		return result;
	}

}
